(set-logic QF_ABV)
(set-info :source |
The benchmarks come from Bounded Model Checking of software.
Contributed by Lorenzo Platania (c1009@unige.it).
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun main_0_head1_0 () (_ BitVec 32))
(declare-fun main_0_head1_1 () (_ BitVec 32))
(assert (= main_0_head1_1 (_ bv0 32)))
(declare-fun arr_val_0 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun arr_val_1 () (Array (_ BitVec 32) (_ BitVec 32)))
(assert (= arr_val_1 (store arr_val_0 main_0_head1_1 (_ bv0 32))))
(declare-fun arr_next_0 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun arr_next_1 () (Array (_ BitVec 32) (_ BitVec 32)))
(assert (= arr_next_1 (store arr_next_0 main_0_head1_1 (bvneg (_ bv1 32)))))
(declare-fun main_0_curr_0 () (_ BitVec 32))
(declare-fun main_0_curr_1 () (_ BitVec 32))
(assert (= main_0_curr_1 main_0_head1_1))
(declare-fun main_0_i_0 () (_ BitVec 32))
(declare-fun main_0_i_1 () (_ BitVec 32))
(assert (= main_0_i_1 (_ bv1 32)))
(declare-fun main_0_tmp_0 () (_ BitVec 32))
(declare-fun main_0_tmp_1 () (_ BitVec 32))
(assert (= main_0_tmp_1 (ite (bvult main_0_i_1 (_ bv4 32)) (_ bv1 32) main_0_tmp_0)))
(declare-fun undefInt_1 () (_ BitVec 32))
(declare-fun arr_val_2 () (Array (_ BitVec 32) (_ BitVec 32)))
(assert (= arr_val_2 (ite (bvult main_0_i_1 (_ bv4 32)) (store arr_val_1 main_0_tmp_1 undefInt_1) arr_val_1)))
(declare-fun arr_next_2 () (Array (_ BitVec 32) (_ BitVec 32)))
(assert (= arr_next_2 (ite (bvult main_0_i_1 (_ bv4 32)) (store arr_next_1 main_0_curr_1 main_0_tmp_1) arr_next_1)))
(declare-fun main_0_curr_2 () (_ BitVec 32))
(assert (= main_0_curr_2 (ite (bvult main_0_i_1 (_ bv4 32)) (select arr_next_2 main_0_curr_1) main_0_curr_1)))
(declare-fun arr_next_3 () (Array (_ BitVec 32) (_ BitVec 32)))
(assert (= arr_next_3 (ite (bvult main_0_i_1 (_ bv4 32)) (store arr_next_2 main_0_tmp_1 (bvneg (_ bv1 32))) arr_next_2)))
(declare-fun main_0_temp_i_0 () (_ BitVec 32))
(declare-fun main_0_temp_i_1 () (_ BitVec 32))
(assert (= main_0_temp_i_1 (ite (bvult main_0_i_1 (_ bv4 32)) main_0_i_1 main_0_temp_i_0)))
(declare-fun main_0_i_2 () (_ BitVec 32))
(assert (= main_0_i_2 (ite (bvult main_0_i_1 (_ bv4 32)) (bvadd main_0_i_1 (_ bv1 32)) main_0_i_1)))
(declare-fun main_0_tmp_2 () (_ BitVec 32))
(assert (= main_0_tmp_2 (ite (bvult main_0_i_2 (_ bv4 32)) (_ bv2 32) main_0_tmp_1)))
(declare-fun undefInt_2 () (_ BitVec 32))
(declare-fun arr_val_3 () (Array (_ BitVec 32) (_ BitVec 32)))
(assert (= arr_val_3 (ite (bvult main_0_i_2 (_ bv4 32)) (store arr_val_2 main_0_tmp_2 undefInt_2) arr_val_2)))
(declare-fun arr_next_4 () (Array (_ BitVec 32) (_ BitVec 32)))
(assert (= arr_next_4 (ite (bvult main_0_i_2 (_ bv4 32)) (store arr_next_3 main_0_curr_2 main_0_tmp_2) arr_next_3)))
(declare-fun main_0_curr_3 () (_ BitVec 32))
(assert (= main_0_curr_3 (ite (bvult main_0_i_2 (_ bv4 32)) (select arr_next_4 main_0_curr_2) main_0_curr_2)))
(declare-fun arr_next_5 () (Array (_ BitVec 32) (_ BitVec 32)))
(assert (= arr_next_5 (ite (bvult main_0_i_2 (_ bv4 32)) (store arr_next_4 main_0_tmp_2 (bvneg (_ bv1 32))) arr_next_4)))
(declare-fun main_0_temp_i_2 () (_ BitVec 32))
(assert (= main_0_temp_i_2 (ite (bvult main_0_i_2 (_ bv4 32)) main_0_i_2 main_0_temp_i_1)))
(declare-fun main_0_i_3 () (_ BitVec 32))
(assert (= main_0_i_3 (ite (bvult main_0_i_2 (_ bv4 32)) (bvadd main_0_i_2 (_ bv1 32)) main_0_i_2)))
(declare-fun main_0_tmp_3 () (_ BitVec 32))
(assert (= main_0_tmp_3 (ite (bvult main_0_i_3 (_ bv4 32)) (_ bv3 32) main_0_tmp_2)))
(declare-fun undefInt_3 () (_ BitVec 32))
(declare-fun arr_val_4 () (Array (_ BitVec 32) (_ BitVec 32)))
(assert (= arr_val_4 (ite (bvult main_0_i_3 (_ bv4 32)) (store arr_val_3 main_0_tmp_3 undefInt_3) arr_val_3)))
(declare-fun arr_next_6 () (Array (_ BitVec 32) (_ BitVec 32)))
(assert (= arr_next_6 (ite (bvult main_0_i_3 (_ bv4 32)) (store arr_next_5 main_0_curr_3 main_0_tmp_3) arr_next_5)))
(declare-fun main_0_curr_4 () (_ BitVec 32))
(assert (= main_0_curr_4 (ite (bvult main_0_i_3 (_ bv4 32)) (select arr_next_6 main_0_curr_3) main_0_curr_3)))
(declare-fun arr_next_7 () (Array (_ BitVec 32) (_ BitVec 32)))
(assert (= arr_next_7 (ite (bvult main_0_i_3 (_ bv4 32)) (store arr_next_6 main_0_tmp_3 (bvneg (_ bv1 32))) arr_next_6)))
(declare-fun main_0_temp_i_3 () (_ BitVec 32))
(assert (= main_0_temp_i_3 (ite (bvult main_0_i_3 (_ bv4 32)) main_0_i_3 main_0_temp_i_2)))
(declare-fun main_0_i_4 () (_ BitVec 32))
(assert (= main_0_i_4 (ite (bvult main_0_i_3 (_ bv4 32)) (bvadd main_0_i_3 (_ bv1 32)) main_0_i_3)))
(declare-fun main_0_tmp_4 () (_ BitVec 32))
(assert (= main_0_tmp_4 (ite (bvult main_0_i_4 (_ bv4 32)) (_ bv4 32) main_0_tmp_3)))
(declare-fun undefInt_4 () (_ BitVec 32))
(declare-fun arr_val_5 () (Array (_ BitVec 32) (_ BitVec 32)))
(assert (= arr_val_5 (ite (bvult main_0_i_4 (_ bv4 32)) (store arr_val_4 main_0_tmp_4 undefInt_4) arr_val_4)))
(declare-fun arr_next_8 () (Array (_ BitVec 32) (_ BitVec 32)))
(assert (= arr_next_8 (ite (bvult main_0_i_4 (_ bv4 32)) (store arr_next_7 main_0_curr_4 main_0_tmp_4) arr_next_7)))
(declare-fun main_0_curr_5 () (_ BitVec 32))
(assert (= main_0_curr_5 (ite (bvult main_0_i_4 (_ bv4 32)) (select arr_next_8 main_0_curr_4) main_0_curr_4)))
(declare-fun arr_next_9 () (Array (_ BitVec 32) (_ BitVec 32)))
(assert (= arr_next_9 (ite (bvult main_0_i_4 (_ bv4 32)) (store arr_next_8 main_0_tmp_4 (bvneg (_ bv1 32))) arr_next_8)))
(declare-fun main_0_temp_i_4 () (_ BitVec 32))
(assert (= main_0_temp_i_4 (ite (bvult main_0_i_4 (_ bv4 32)) main_0_i_4 main_0_temp_i_3)))
(declare-fun main_0_i_5 () (_ BitVec 32))
(assert (= main_0_i_5 (ite (bvult main_0_i_4 (_ bv4 32)) (bvadd main_0_i_4 (_ bv1 32)) main_0_i_4)))
(declare-fun main_0_tmp_5 () (_ BitVec 32))
(assert (= main_0_tmp_5 (ite (bvult main_0_i_5 (_ bv4 32)) (_ bv5 32) main_0_tmp_4)))
(declare-fun undefInt_5 () (_ BitVec 32))
(declare-fun arr_val_6 () (Array (_ BitVec 32) (_ BitVec 32)))
(assert (= arr_val_6 (ite (bvult main_0_i_5 (_ bv4 32)) (store arr_val_5 main_0_tmp_5 undefInt_5) arr_val_5)))
(declare-fun arr_next_10 () (Array (_ BitVec 32) (_ BitVec 32)))
(assert (= arr_next_10 (ite (bvult main_0_i_5 (_ bv4 32)) (store arr_next_9 main_0_curr_5 main_0_tmp_5) arr_next_9)))
(declare-fun main_0_curr_6 () (_ BitVec 32))
(assert (= main_0_curr_6 (ite (bvult main_0_i_5 (_ bv4 32)) (select arr_next_10 main_0_curr_5) main_0_curr_5)))
(declare-fun arr_next_11 () (Array (_ BitVec 32) (_ BitVec 32)))
(assert (= arr_next_11 (ite (bvult main_0_i_5 (_ bv4 32)) (store arr_next_10 main_0_tmp_5 (bvneg (_ bv1 32))) arr_next_10)))
(declare-fun main_0_temp_i_5 () (_ BitVec 32))
(assert (= main_0_temp_i_5 (ite (bvult main_0_i_5 (_ bv4 32)) main_0_i_5 main_0_temp_i_4)))
(declare-fun main_0_i_6 () (_ BitVec 32))
(assert (= main_0_i_6 (ite (bvult main_0_i_5 (_ bv4 32)) (bvadd main_0_i_5 (_ bv1 32)) main_0_i_5)))
(assert (not (=> (bvult main_0_i_5 (_ bv4 32)) (not (bvult main_0_i_6 (_ bv4 32))))))
(check-sat)
